\section{Enunciado e Introducci'on}

\subsection{Extracto del enunciado}

Dado un conjunto de cl'ausulas en forma normal disyuntiva, el problema MAX-SAT consiste
en encontrar una asignaci'on de verdad de las variables presentes de tal modo que se satisfaga
la mayor cantidad posible de cl'ausulas.

\subsection{Introduccion Te'orica}
El problema al cual nos vamos a abocar es MAX-SAT. Se trata de un problema de m'axima satisfabilidad.\\
Que consiste en determinar si una variable puede ser asignada en una f'ormula booleana de tal forma que al evaluar dicha f'ormula sea verdadera.\\
Se basa en obtener el m'aximo n'umero de f'ormulas booleanas safisfechas, a partir de una asignaci'on arbitaria del valor de los literales de la instancia del problema.
%Aca tenemos que poner 2 ejemplos, uno que valide un par de cl'ausulas y otro que haga el maximo

\subsection{Objetivo}
El objetivo de este informe es aplicar diferentes t'ecnicas algori'timcas, algoritmo exacto y diversas heuri'sticas, al problema MAX-SAT y comparar los resultados emp'iricamente para elaborar conclusiones respecto a dichas t'ecnicas.\\
Cuando se haga referencia a \textbf{la mejor soluci'on} se est'a hablando de aquella que maximiza el problema propuesto. Hay muchas soluciones v'alidas para este problema pero no todas hacen m'axima la cantidad de cl'asulas satisfechas.\\
Se plantearon las siguientes soluciones:

\begin{itemize}
%basado en la t'ecnica de \textit{BackTracking}
	\item Un algoritmo exacto, determin'istico, que busca la mejor soluci'on aplicando fuerza bruta (recorriendo todas las soluciones) con cierta inteligencia en lo concerniente a la aplicaci'on de \textit{podas} para dicho algoritmo. El problema del algoritmo propuesto es su complejidad temporal, ya que es exponencial. Para problemas con muchas variables y cl'ausulas es inviable, por lo tanto se intentan aplicar heur'isticas.
	\item Una heur'istica constructiva, basada en la t'ecnica de algoritmos \textit{golosos} que intenta aproximarse a la mejor soluci'on en forma \textit{r'apida} (complejidad temporal polinomial). El problema de esta heur'istica es que hay casos en los que no encuentra la mejor soluci'on y hay otros en los que est'a muy alejado de la misma.
	\item Una \textit{heur'istica de b'usqueda local}, la cual consiste en variar de cierta manera la soluci'on propuesta por la heur'istica constructiva y generar una \textit{vecindad} de soluciones para explorar y quedarse con la mejor. El problema est'a en que buscamos soluciones nuevas acotadas en un dominio dado por el cambio que hicimos a la soluci'on inicial sin explorar otras soluciones que podr'ian ser potencialmente buenas.
	\item Finalmente, la \textit{heur'istica b'usqueda Tab'u (Tabu Search)}, que plantea una mejora considerable respecto de la B'usqueda Local ya que permite encontrar nuevas soluciones, mediante la exploracion de diversas vecindades ampliando el dominio tan restringido de la b'usqueda local.
\end{itemize}

\subsection{Consideraciones generales}

Vamos a definir los siguientes elementos que se repetiran a lo largo del informe:
\begin{itemize}
	\item Sea CasoDePrueba una Tupla compuesta por: $\langle$ Lista $\langle$ Clausulas $\rangle$ x Cantidad de Variables x Cantidad de Clausulas $\rangle$.
	\item Sea $v$ la cantidad de variables de un caso de prueba.
	\item Sea $c$ la cantidad de variables de un caso de prueba.
	\item Sea $V$ vector de tama'no $v$ donde $V_i \in {0,1}$, este vector representa una posible soluci'on al problema MAX-SAT, donde el elemento $i$-'esimo est'a presente en una posible soluci'on. Entonces si el valor de la posicion $V_i = 1$, significa que en la soluci'on a evaluar, el valor de la variable $i$ esta no negado, en cambio si es $V_i = 0$ el valor en la solucion esta negada.
\end{itemize}

 

